Merge the scalar and element marshallers into ReadZ3Value - #109
Draft
HowardvanRooijen wants to merge 1 commit into
Draft
Merge the scalar and element marshallers into ReadZ3Value#109HowardvanRooijen wants to merge 1 commit into
HowardvanRooijen wants to merge 1 commit into
Conversation
Reading a solved symbol back from the model was written twice - once for a scalar member, once per collection element - as two ~35-line switch statements that were arm-for-arm identical: the same casts, the same checked conversions, the same decimal-string handling, differing only in which Expr they read and which "unsupported type" message they threw. One `ReadZ3Value` now owns the reader, and a small `ParseZ3Decimal` owns the shared trailing-'?' decimal parse. Net -64 lines, and a type that reads back wrong now has one place to fix rather than two to keep in step. The element path passes its element type so the array-specific diagnostic is preserved; a null there selects the scalar message. The collection loop reads its element type code once now, rather than on every element. Behaviour-preserving: - 322 tests unchanged. - A mutation of the shared Int32 arm (+1) fails 111 tests, across both the scalar and the collection paths - the reader is exercised, and a regression in it is caught. - Allocation unchanged (the per-arm boxing is the same), confirmed with the benchmark suite: every shape within run-to-run rounding of its prior figure. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PipoHZJsgydrV3JC3fQN6Q
Test Results 1 files 1 suites 10s ⏱️ Results for commit 8f0659d. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Third and largest of the three flagged dedup refactors, and the one worth the most: reading a solved
symbol back from the Z3 model was written twice - once for a scalar member, once per collection
element - as two ~35-line
switch (typeCode)statements that were arm-for-arm identical. Same casts,same checked integer conversions, same
DateTime-from-ticks, same trailing-?decimal-string parse;they differed only in which
Exprthey read (valvs the selected element) and which "unsupportedtype" message they threw.
One
ReadZ3Value(Expr, TypeCode, symbolName, elementType)now owns the reader, and a smallParseZ3Decimalowns the shared decimal parse. Net -64 lines, and a type that reads back wrong nowhas one place to fix rather than two that had to be kept in lock-step (exactly the kind of drift that
produced #55).
nullthere selects the scalar message. No test couples to either message, but both are kept exactly.
Verified
dotnet build solutions/Z3.Linq.slnx -c Release- clean,TreatWarningsAsErrorsand documentationgeneration on.
identical pass is the behaviour-preservation evidence.
Int32arm (+ 1) fails 111 tests, spanning both thescalar and the collection paths - the merged reader is genuinely exercised, and a regression in it
is caught.
Z3.Linq.Benchmarks(short job,
MemoryDiagnoser): every shape within run-to-run rounding of its prior figure(Collection 4.57 KB, ScalarSymbols 3.30 KB, ...).
./build.ps1 -Configuration Release- 46 tasks, 0 errors, 0 warnings.No public-API or behaviour change - an internal readability/maintainability refactor. Releases remain
on hold under #60 regardless.
🤖 Generated with Claude Code